Termination proof of /tmp/tmpobgrRG/Ex9

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))

The replacement map contains the following entries:

filter: {1, 2, 3}
cons: {1}
0: empty set
s: {1}
sieve: {1}
nats: {1}
zprimes: empty set

↳ CSR

  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))

The replacement map contains the following entries:

filter: {1, 2, 3}
cons: {1}
0: empty set
s: {1}
sieve: {1}
nats: {1}
zprimes: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))

The replacement map contains the following entries:

filter: {1, 2, 3}
cons: {1}
0: empty set
s: {1}
sieve: {1}
nats: {1}
zprimes: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {filter, s, sieve, nats, SIEVE, NATS, FILTER} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

ZPRIMES → SIEVE(nats(s(s(0))))
ZPRIMES → NATS(s(s(0)))

The hidden terms of R are:

filter(Y, M, M)
filter(Y, N, M)
sieve(Y)
sieve(filter(Y, N, N))
filter(Y, N, N)
nats(s(N))

Every hiding context is built from:

filter on positions {1, 2, 3}
sieve on positions {1}
s on positions {1}
nats on positions {1}

Hence, the new unhiding pairs DP_u are :

U(filter(x_0, x_1, x_2)) → U(x_0)
U(filter(x_0, x_1, x_2)) → U(x_1)
U(filter(x_0, x_1, x_2)) → U(x_2)
U(sieve(x_0)) → U(x_0)
U(s(x_0)) → U(x_0)
U(nats(x_0)) → U(x_0)
U(filter(Y, M, M)) → FILTER(Y, M, M)
U(filter(Y, N, M)) → FILTER(Y, N, M)
U(sieve(Y)) → SIEVE(Y)
U(sieve(filter(Y, N, N))) → SIEVE(filter(Y, N, N))
U(nats(s(N))) → NATS(s(N))

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))

The set Q consists of the following terms:

filter(cons(x0, x1), 0, x2)
filter(cons(x0, x1), s(x2), x3)
sieve(cons(0, x0))
sieve(cons(s(x0), x1))
nats(x0)
zprimes

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 5 less nodes.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ QCSDP

              ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {filter, s, sieve, nats} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(filter(x_0, x_1, x_2)) → U(x_0)
U(filter(x_0, x_1, x_2)) → U(x_1)
U(filter(x_0, x_1, x_2)) → U(x_2)
U(sieve(x_0)) → U(x_0)
U(s(x_0)) → U(x_0)
U(nats(x_0)) → U(x_0)

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))

The set Q consists of the following terms:

filter(cons(x0, x1), 0, x2)
filter(cons(x0, x1), s(x2), x3)
sieve(cons(0, x0))
sieve(cons(s(x0), x1))
nats(x0)
zprimes

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(filter(x_0, x_1, x_2)) → U(x_0)
U(filter(x_0, x_1, x_2)) → U(x_1)
U(filter(x_0, x_1, x_2)) → U(x_2)
U(sieve(x_0)) → U(x_0)
U(s(x_0)) → U(x_0)
U(nats(x_0)) → U(x_0)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ QCSDP

              ↳ QCSDPSubtermProof

                ↳ QCSDP

                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {filter, s, sieve, nats} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))

The set Q consists of the following terms:

filter(cons(x0, x1), 0, x2)
filter(cons(x0, x1), s(x2), x3)
sieve(cons(0, x0))
sieve(cons(s(x0), x1))
nats(x0)
zprimes

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.